i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), T:Type, es:event_system{i:l}.
es-decls(es;i;ds;da)
 subtype_rel(es-vartype(es; i; mkid{ecl:ut2}); T)
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 es-decls(es;i;fpf-join(id-deq; ds; fpf-single(mkid{ecl:ut2}; T));da) 

latex

Definitions	guard(T), P  Q, P  Q, P  Q, x:A. B(x), x. t(x), P  Q, t  T, Id, mkid{$x:ut2}, if b then t else f fi , tt, top, ff, prop{i:l}, fpf-cap(f; eq; x; z), t.2, fpf-single(x; v), fpf-ap(f; eq; x), sq_type(T), x(s), Unit, ,
Lemmas	es-decls-iff, fpf-single wf, es-vartype wf, fpf-join wf, fpf-compatible-join-cap, fpf-compatible-single, id-deq wf, top wf, fpf-dom wf, iff transitivity, bool wf, assert wf, bnot wf, eqtt to assert, eqff to assert, assert of bnot, not wf, Id sq, fpf-single-dom